Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen.

Ja, wir steigen jetzt tiefer ein in die Prädikatenlogik 1. Stufe, die wir letztes Mal

kennengelernt haben. Wir gehen umgekehrt vor wie bei der Aussagenlogik. Bei der Aussagenlogik

haben wir uns nach Einführung der Syntax ja zunächst die Semantik angesehen und dann

ein Beweissystem eingeführt. Unter anderem deswegen, weil die Semantik eben einfacher

zu verstehen ist als das Beweissystem. Das ist nun bei der Logik 1. Stufe genau umgekehrt.

Die Regeln sind jetzt nicht so schockierend, die wir gleich sehen. Wir machen also das

Schlusssystem, also das System natürlich entschließend erst. Wir erweitern schlicht

dann einfach das, was wir für propositionale Logik schon haben. Das heißt, so viele an

neuen Konstrukten haben wir jetzt ja gar nicht abzudecken, nur Gleichheit und die Quantoren.

Und wie gesagt, die Regeln sind eigentlich relativ straightforward, bis auf vielleicht

eine. Während die Semantik der Logik 1. Stufe doch, naja, auch allein so von den Datenstrukturen

doch so ein bisschen komplizierter ist und vielleicht auch so ein bisschen mehr an Abstraktionsvermögen

noch verlangt. Gut, das heißt, achso, ja, und ich kündige gleich an, wie letztes Mal

begleite ich also die, was heißt begleiten, also ich schließe an an die Einführung dieses

Systems eine Demo in Coq. Ich hatte oft, also optimistischerweise nur ein HDMI-Adapter dabei,

deswegen kommt hoffentlich gleich noch unsere Administratorin und bringt einen VGA-Adapter,

daher auch das Telefonat. Gut, und ja, wir werden jetzt also einfach beginnen mit dieser

Einführung in Folgendes. Gut, ja, wie gesagt, wir müssen also im Grunde nur für unsere

neuen Konstrukte noch Einführungs- und Eliminationsregeln hinzufügen. Wir verwenden also das alte System

mit. Wir fangen an mit den Regeln für Gleichheit, die werden uns auch gar nicht so in erster

Linie beschäftigen und sie sind auch beide recht einfach. Wir haben also eine Einführungsregel

für Gleichheit. Ja, das fällt einem ein, wann kann ich irgendwie eine Gleichheit hinschreiben?

Nun, ganz sicher dann, wenn ich links und rechts denselben Term hinschreibe. Jeder Term

E ist ganz sicher gleich sich selbst, also das ist unsere Einführungsregel für Gleichheit.

Und dann haben wir auch nur eine Eliminationsregel, die ist von ihrer Natur her vielleicht ein

bisschen überraschend, also sie ist nicht schwer zu verstehen oder sowas, es ist nur

überraschend, dass das alles sein soll. Also, wir stellen uns vor, für irgendeinen Term

E würde eine Aussage Phi gelten. Wie drücken wir das syntaktisch aus? Nun, syntaktisch

drücken wir das dadurch aus, dass wir sagen, gut, Phi hat halt eine freie Variable X, womöglich,

vielleicht auch nicht. Und für diese freie Variable X substituieren wir diesen Term E

und das drückt uns dann aus, dass dieser Term E eben Phi erfüllt. So, und außerdem stellen

wir uns vor, wir hätten hier geleitet, dieser Term E für den Phi gilt ja seinem gleich

einem anderen Term D. Nun, wenn das so ist, würden wir niemals widersprechen, wenn ich

behaupte, dann gilt Phi sicher auch für D, denn D ist ja nunmal dasselbe wie E und Phi

gilt ja für E. So, und das ist schon alles. So, nun stellt man sich ja von Gleichheit

eigentlich so instinktiv vor, dass sie noch ein paar andere Eigenschaften hat. Ich habe

gewissermaßen hingeschrieben, Gleichheit sei transitiv. Nun, man wird auch außerdem vermuten,

dass Gleichheit vielleicht auch noch symmetrisch und transitiv ist, nicht? Also, das bietet

man sich ja immer so her, nicht? Also, zum Beispiel ja, wenn zwei Dinge untereinander

gleich sind, wie war das noch? Und der zweite ist zweiter, ein drittengleich ist auch das

erste, ein drittengleich oder sowas. Ja, es gibt irgendwie so Merksprüche aus der Mittelstufe.

Erwartet man schon, dass das hier kommt, nicht? Und das kommt nun aber nicht. Nun ja, also

zum Beispiel, nicht? Dieser Regel hier, Symmetrie, die würde man natürlich gerne haben, ja?

Ich mache jetzt hier mal einen großen waagerechten Strich, um einzudeuten, dass das eigentliche

Beweissystem, jedenfalls soweit Gleichheit betroffen ist, jetzt zu Ende ist. Ja, sieht

jemand, wo das herkommt? Muss ja irgendwie gehen, nicht? Denn ich meine, sonst wäre ja

unser Beweissystem jetzt unvollständig und zumindest mal auf der einfachen Ebene der

Gleichheit wollen wir das sicher nicht. Naja, also wir haben zur Verfügung nur diese beiden